
import sys, itertools, re

from optparse import OptionParser


def _mta( literals, davidsonianize, f_no_cost = False, cost_coe = 100 ):

	ret = []
	non_merge_pool = set()
	
	for literal in literals:
		literal   = [x.strip() for x in re.split( "[():,]", literal )]
		arguments = literal[1: (-2 if not f_no_cost else len(literal)-1 ) ]

		# inst replacement
		if "inst" == literal[0]:
			literal[0] = arguments[1][ (0 if 1 == cost_coe else 1) :]
			arguments.remove( arguments[1] )

		# Name the constant arguments
		for i in xrange( len( arguments ) ):
			arguments[i] = arguments[i].replace( "-", "'" )
			
			if (arguments[i] in ["+busdriver", "+taxidriver"]) or (1 == cost_coe and arguments[i] in ["busdriver", "taxidriver"]):
				if not davidsonianize.has_key( arguments[i] ):
					davidsonianize[ arguments[i] ] = "c%d" % (1+len(davidsonianize))

					if 1 == cost_coe:
						ret += [ "%s(%s):%d:%d:0:{}" % (arguments[i], davidsonianize[ arguments[i] ], 100+len(ret), int( cost_coe * float(literal[-1])) if not f_no_cost else 0 ) ]
					else:
						ret += ["%s(%s):%s" % (arguments[i][1:], davidsonianize[ arguments[i] ],  int( cost_coe * float(literal[-1])) if not f_no_cost else 0 ) ]
					
				arguments[i] = davidsonianize[ arguments[i] ]

		if 1 == cost_coe:
			ret += [ "%s(%s):%d:%d:0:{}" % ( literal[0], ",".join( arguments ), len(ret), int( cost_coe * float(literal[-1])) if not f_no_cost else 0 ) ]
		else:
			ret += [ "%s(%s):%s" % ( literal[0], ",".join( arguments ), int( cost_coe * float(literal[-1])) if not f_no_cost else 0 ) ]
			
		non_merge_pool |= set( arguments )
	
	return " & ".join( ret ), ",".join( ["%s-%s" % c for c in itertools.combinations( non_merge_pool, 2 ) if c[0]!=c[1] ] )


def main():

	axiom_counter = 1
	op = OptionParser()
	# op.add_option( "-i", "--mini-tacitus-format", dest="mini_tac", action="store_true" )

	options, args = op.parse_args()

	if 1 != len( args ): op.error( "Wrong parameters." )
	
	for ln in open( args[0] ):

		if "" == ln.strip(): continue

		if ln.startswith( "#" ):
			ln = ln.rstrip().split("\t")

			if 2 != len(ln): continue

			ln = ln[1]

		clause = ln.rstrip().split( "=>" )
		david  = {}

		if 2 == len( clause ):
			lhs, rhs = _mta( re.split( "[&^]", clause[0] ), david ), _mta( re.split( "[&^]", clause[1] ), david, f_no_cost=True )
			print "%d]" % axiom_counter, lhs[0], "->", rhs[0] + " | "
		else:
			ret, nmp = _mta( re.split( "[&^]", clause[0] ), david, cost_coe = 1 )
			print "%d]" % axiom_counter, ret + " |" + nmp + "| "

		axiom_counter += 1
		

if "__main__" == __name__: main()
